Conversation
|
looks good |
The CI errors seem to be due to tentative compilations agains MathComp 2.2.0, in which, indeed, The last commit tentatively drops MathComp 2.2.0 @proux01 @CohenCyril |
It's enough to fix the opam file, the nix configuration also needs to be changed apparently, but then I'm clueless. Do you happen to know now that you've been fixing Infotheo's files? |
|
For nix, just edit that line:; Line 54 in 7528cc1 (you can even remove the line entirely if you want to require 2.4.0 since it's the default with Coq 8.20, according to https://github.com/NixOS/nixpkgs/blob/8c312f9b188a5a082b9062e8d54e8e9aed4e3804/pkgs/development/coq-modules/mathcomp/default.nix#L38 ) |
Thanks. I was looking only at the |
| bundles."8.20".coqPackages = common-bundle // { | ||
| coq.override.version = "8.20"; | ||
| mathcomp.override.version = "2.2.0"; | ||
| mathcomp.override.version = "2.3.0"; |
There was a problem hiding this comment.
we should also be testing mathcomp 2.4.0
There was a problem hiding this comment.
I will open a new PR for that.
There was a problem hiding this comment.
It's already tested in the 9.0 bundle, that's probably enough?
There was a problem hiding this comment.
There can be some weird things happening when combining different versions. I would not be willing to try my luck with the last version of mathcomp.
* rm forms.v
4 participants
Motivation for this change
Checklist
CHANGELOG_UNRELEASED.md- [ ] added corresponding documentation in the headersReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers